Left Termination of the query pattern dis_in_1(g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

dis(or(B1, B2)) :- ','(con(B1), dis(B2)).
dis(B) :- con(B).
con(and(B1, B2)) :- ','(dis(B1), con(B2)).
con(B) :- bool(B).
bool(0).
bool(1).

Queries:

dis(g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

dis_in(B) → U3(B, con_in(B))
con_in(B) → U6(B, bool_in(B))
bool_in(1) → bool_out(1)
bool_in(0) → bool_out(0)
U6(B, bool_out(B)) → con_out(B)
con_in(and(B1, B2)) → U4(B1, B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B1, B2, con_in(B1))
U1(B1, B2, con_out(B1)) → U2(B1, B2, dis_in(B2))
U2(B1, B2, dis_out(B2)) → dis_out(or(B1, B2))
U4(B1, B2, dis_out(B1)) → U5(B1, B2, con_in(B2))
U5(B1, B2, con_out(B2)) → con_out(and(B1, B2))
U3(B, con_out(B)) → dis_out(B)

The argument filtering Pi contains the following mapping:
dis_in(x1)  =  dis_in(x1)
U3(x1, x2)  =  U3(x2)
con_in(x1)  =  con_in(x1)
U6(x1, x2)  =  U6(x2)
bool_in(x1)  =  bool_in(x1)
1  =  1
bool_out(x1)  =  bool_out
0  =  0
con_out(x1)  =  con_out
and(x1, x2)  =  and(x1, x2)
U4(x1, x2, x3)  =  U4(x2, x3)
or(x1, x2)  =  or(x1, x2)
U1(x1, x2, x3)  =  U1(x2, x3)
U2(x1, x2, x3)  =  U2(x3)
dis_out(x1)  =  dis_out
U5(x1, x2, x3)  =  U5(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

dis_in(B) → U3(B, con_in(B))
con_in(B) → U6(B, bool_in(B))
bool_in(1) → bool_out(1)
bool_in(0) → bool_out(0)
U6(B, bool_out(B)) → con_out(B)
con_in(and(B1, B2)) → U4(B1, B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B1, B2, con_in(B1))
U1(B1, B2, con_out(B1)) → U2(B1, B2, dis_in(B2))
U2(B1, B2, dis_out(B2)) → dis_out(or(B1, B2))
U4(B1, B2, dis_out(B1)) → U5(B1, B2, con_in(B2))
U5(B1, B2, con_out(B2)) → con_out(and(B1, B2))
U3(B, con_out(B)) → dis_out(B)

The argument filtering Pi contains the following mapping:
dis_in(x1)  =  dis_in(x1)
U3(x1, x2)  =  U3(x2)
con_in(x1)  =  con_in(x1)
U6(x1, x2)  =  U6(x2)
bool_in(x1)  =  bool_in(x1)
1  =  1
bool_out(x1)  =  bool_out
0  =  0
con_out(x1)  =  con_out
and(x1, x2)  =  and(x1, x2)
U4(x1, x2, x3)  =  U4(x2, x3)
or(x1, x2)  =  or(x1, x2)
U1(x1, x2, x3)  =  U1(x2, x3)
U2(x1, x2, x3)  =  U2(x3)
dis_out(x1)  =  dis_out
U5(x1, x2, x3)  =  U5(x3)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DIS_IN(B) → U31(B, con_in(B))
DIS_IN(B) → CON_IN(B)
CON_IN(B) → U61(B, bool_in(B))
CON_IN(B) → BOOL_IN(B)
CON_IN(and(B1, B2)) → U41(B1, B2, dis_in(B1))
CON_IN(and(B1, B2)) → DIS_IN(B1)
DIS_IN(or(B1, B2)) → U11(B1, B2, con_in(B1))
DIS_IN(or(B1, B2)) → CON_IN(B1)
U11(B1, B2, con_out(B1)) → U21(B1, B2, dis_in(B2))
U11(B1, B2, con_out(B1)) → DIS_IN(B2)
U41(B1, B2, dis_out(B1)) → U51(B1, B2, con_in(B2))
U41(B1, B2, dis_out(B1)) → CON_IN(B2)

The TRS R consists of the following rules:

dis_in(B) → U3(B, con_in(B))
con_in(B) → U6(B, bool_in(B))
bool_in(1) → bool_out(1)
bool_in(0) → bool_out(0)
U6(B, bool_out(B)) → con_out(B)
con_in(and(B1, B2)) → U4(B1, B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B1, B2, con_in(B1))
U1(B1, B2, con_out(B1)) → U2(B1, B2, dis_in(B2))
U2(B1, B2, dis_out(B2)) → dis_out(or(B1, B2))
U4(B1, B2, dis_out(B1)) → U5(B1, B2, con_in(B2))
U5(B1, B2, con_out(B2)) → con_out(and(B1, B2))
U3(B, con_out(B)) → dis_out(B)

The argument filtering Pi contains the following mapping:
dis_in(x1)  =  dis_in(x1)
U3(x1, x2)  =  U3(x2)
con_in(x1)  =  con_in(x1)
U6(x1, x2)  =  U6(x2)
bool_in(x1)  =  bool_in(x1)
1  =  1
bool_out(x1)  =  bool_out
0  =  0
con_out(x1)  =  con_out
and(x1, x2)  =  and(x1, x2)
U4(x1, x2, x3)  =  U4(x2, x3)
or(x1, x2)  =  or(x1, x2)
U1(x1, x2, x3)  =  U1(x2, x3)
U2(x1, x2, x3)  =  U2(x3)
dis_out(x1)  =  dis_out
U5(x1, x2, x3)  =  U5(x3)
U51(x1, x2, x3)  =  U51(x3)
U61(x1, x2)  =  U61(x2)
U41(x1, x2, x3)  =  U41(x2, x3)
CON_IN(x1)  =  CON_IN(x1)
BOOL_IN(x1)  =  BOOL_IN(x1)
U31(x1, x2)  =  U31(x2)
DIS_IN(x1)  =  DIS_IN(x1)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x2, x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

DIS_IN(B) → U31(B, con_in(B))
DIS_IN(B) → CON_IN(B)
CON_IN(B) → U61(B, bool_in(B))
CON_IN(B) → BOOL_IN(B)
CON_IN(and(B1, B2)) → U41(B1, B2, dis_in(B1))
CON_IN(and(B1, B2)) → DIS_IN(B1)
DIS_IN(or(B1, B2)) → U11(B1, B2, con_in(B1))
DIS_IN(or(B1, B2)) → CON_IN(B1)
U11(B1, B2, con_out(B1)) → U21(B1, B2, dis_in(B2))
U11(B1, B2, con_out(B1)) → DIS_IN(B2)
U41(B1, B2, dis_out(B1)) → U51(B1, B2, con_in(B2))
U41(B1, B2, dis_out(B1)) → CON_IN(B2)

The TRS R consists of the following rules:

dis_in(B) → U3(B, con_in(B))
con_in(B) → U6(B, bool_in(B))
bool_in(1) → bool_out(1)
bool_in(0) → bool_out(0)
U6(B, bool_out(B)) → con_out(B)
con_in(and(B1, B2)) → U4(B1, B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B1, B2, con_in(B1))
U1(B1, B2, con_out(B1)) → U2(B1, B2, dis_in(B2))
U2(B1, B2, dis_out(B2)) → dis_out(or(B1, B2))
U4(B1, B2, dis_out(B1)) → U5(B1, B2, con_in(B2))
U5(B1, B2, con_out(B2)) → con_out(and(B1, B2))
U3(B, con_out(B)) → dis_out(B)

The argument filtering Pi contains the following mapping:
dis_in(x1)  =  dis_in(x1)
U3(x1, x2)  =  U3(x2)
con_in(x1)  =  con_in(x1)
U6(x1, x2)  =  U6(x2)
bool_in(x1)  =  bool_in(x1)
1  =  1
bool_out(x1)  =  bool_out
0  =  0
con_out(x1)  =  con_out
and(x1, x2)  =  and(x1, x2)
U4(x1, x2, x3)  =  U4(x2, x3)
or(x1, x2)  =  or(x1, x2)
U1(x1, x2, x3)  =  U1(x2, x3)
U2(x1, x2, x3)  =  U2(x3)
dis_out(x1)  =  dis_out
U5(x1, x2, x3)  =  U5(x3)
U51(x1, x2, x3)  =  U51(x3)
U61(x1, x2)  =  U61(x2)
U41(x1, x2, x3)  =  U41(x2, x3)
CON_IN(x1)  =  CON_IN(x1)
BOOL_IN(x1)  =  BOOL_IN(x1)
U31(x1, x2)  =  U31(x2)
DIS_IN(x1)  =  DIS_IN(x1)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x2, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 5 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

DIS_IN(or(B1, B2)) → CON_IN(B1)
DIS_IN(or(B1, B2)) → U11(B1, B2, con_in(B1))
DIS_IN(B) → CON_IN(B)
U41(B1, B2, dis_out(B1)) → CON_IN(B2)
CON_IN(and(B1, B2)) → DIS_IN(B1)
U11(B1, B2, con_out(B1)) → DIS_IN(B2)
CON_IN(and(B1, B2)) → U41(B1, B2, dis_in(B1))

The TRS R consists of the following rules:

dis_in(B) → U3(B, con_in(B))
con_in(B) → U6(B, bool_in(B))
bool_in(1) → bool_out(1)
bool_in(0) → bool_out(0)
U6(B, bool_out(B)) → con_out(B)
con_in(and(B1, B2)) → U4(B1, B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B1, B2, con_in(B1))
U1(B1, B2, con_out(B1)) → U2(B1, B2, dis_in(B2))
U2(B1, B2, dis_out(B2)) → dis_out(or(B1, B2))
U4(B1, B2, dis_out(B1)) → U5(B1, B2, con_in(B2))
U5(B1, B2, con_out(B2)) → con_out(and(B1, B2))
U3(B, con_out(B)) → dis_out(B)

The argument filtering Pi contains the following mapping:
dis_in(x1)  =  dis_in(x1)
U3(x1, x2)  =  U3(x2)
con_in(x1)  =  con_in(x1)
U6(x1, x2)  =  U6(x2)
bool_in(x1)  =  bool_in(x1)
1  =  1
bool_out(x1)  =  bool_out
0  =  0
con_out(x1)  =  con_out
and(x1, x2)  =  and(x1, x2)
U4(x1, x2, x3)  =  U4(x2, x3)
or(x1, x2)  =  or(x1, x2)
U1(x1, x2, x3)  =  U1(x2, x3)
U2(x1, x2, x3)  =  U2(x3)
dis_out(x1)  =  dis_out
U5(x1, x2, x3)  =  U5(x3)
U41(x1, x2, x3)  =  U41(x2, x3)
CON_IN(x1)  =  CON_IN(x1)
DIS_IN(x1)  =  DIS_IN(x1)
U11(x1, x2, x3)  =  U11(x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

DIS_IN(or(B1, B2)) → CON_IN(B1)
DIS_IN(B) → CON_IN(B)
DIS_IN(or(B1, B2)) → U11(B2, con_in(B1))
U11(B2, con_out) → DIS_IN(B2)
CON_IN(and(B1, B2)) → DIS_IN(B1)
U41(B2, dis_out) → CON_IN(B2)
CON_IN(and(B1, B2)) → U41(B2, dis_in(B1))

The TRS R consists of the following rules:

dis_in(B) → U3(con_in(B))
con_in(B) → U6(bool_in(B))
bool_in(1) → bool_out
bool_in(0) → bool_out
U6(bool_out) → con_out
con_in(and(B1, B2)) → U4(B2, dis_in(B1))
dis_in(or(B1, B2)) → U1(B2, con_in(B1))
U1(B2, con_out) → U2(dis_in(B2))
U2(dis_out) → dis_out
U4(B2, dis_out) → U5(con_in(B2))
U5(con_out) → con_out
U3(con_out) → dis_out

The set Q consists of the following terms:

dis_in(x0)
con_in(x0)
bool_in(x0)
U6(x0)
U1(x0, x1)
U2(x0)
U4(x0, x1)
U5(x0)
U3(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: